\chapter{Contextual transformations}
In this chapter we introduce one of the most advanced feature of K, the \textit{context transformations}, which gives K an additional degree of modularity.  The process of context transformation is concerned with automatically modifying existing K rules according to the cell structure defined by the desired configuration of a target language. The benefit of context transformation is that it allows us to define semantic rules more abstractly, without worrying about the particular details of the concrete final language configuration.  This way, it implicitly enhances the modularity and reuse of language definitions: existing rules do not need to change as the configuration of the languages changes to accommodate additional language features, and language features defined generically once and for all can be reused across different languages with different configuration structures. \cite{jlap2010}\\
\section{Contextual transformations explained by example}
This section contains some examples of K rules and their corresponding contexts  (or rewrite rules) in order to explain better the transformation process and the aspects we have to consider when giving formal definitions.\\
First, the thread creation rule from SIMPLE semantics (which can be found in the Appendix) is given as the basic example of what is contextual transformations.
\begin{figure}[h]
\centering
\begin{tabular}{| c |}
\hline
\begin{minipage}{.8\textwidth}
\footnotesize
\begin{alltt}
rule     <thread_> 
                \textcolor{red}{<k> spawn S => . <_/k> <env> Env </env> }
         <_/thread>
   (. => <thread_> 
               \textcolor{red}{<k> S </k> <env> Env </env>} 
         <_/thread>)
\end{alltt}
\end{minipage}\\
\hline
\end{tabular}
\caption{Thread creation rule - SIMPLE semantics}
\label{thread:one}
\end{figure}
As we can observe in Figure \ref{thread:one}, it contains only the cells {\it thread}, {\it k} and {\it env}. When in a {\it thread} cell the \verb=spawn S= statement has to be executed then a new thread is created having the instruction set \verb=S= and the same environment \verb=Env= as its creator thread. 
\begin{figure}[h]
\centering
\begin{tabular}{| c |}
\hline
\begin{minipage}{.8\textwidth}
\footnotesize
\begin{alltt}
rule <T>
        <threads>
          <thread_> 
                \textcolor{red}{ <k> spawn S => . <_/k> <env> Env </env> } 
           <_/thread>                                
        (. => <thread_> 
                 \textcolor{red}{<k> S </k> <env> Env </env>}                                                                               
            <_/thread>)
        </threads>
     </T> 
\end{alltt}
\end{minipage}\\
\hline
\end{tabular}
\caption{Thread creation rule full context - SIMPLE semantics}
\label{none}
\end{figure}
The given rule is a K rule in the sense the it is not yet a rewrite rule which is ready to be executed by a rewrite engine. The contextual transformation should add here the missing cells from configuration until the rule matches the configuration and the rewrite can succeed. So, in order to get the context of the rule shown in Figure \ref{thread:one} {\it context transformers} algorithm should receive as input that rule and should output the rule shown in Figure \ref{none}. As we can observe two other cells were added. Actually there were added as many cells as needed in order to fit the configuration. 
In SIMPLE configuration cells {\it T} and {\it threads} are nested and {\it thread} is directly a child of {\it threads}. In the resulted rule the nesting {\it T}-{\it threads} is on the top of the two {\it thread} cells from initial rule. Note that contextual transformations is not only about adding cells on the top of the rule; it has to add all the missing cells. This situation will be better explained in the next example.
Even if it seems very easy to look in the configuration to add the missing cells until the top cell is reached the context transformers have to care about left and right hand side of the rule. The left hand side (also called the lhs) is that part of the rule followed by "=>", while the part of the rule which is preceded by "=>" is considered to be right hand side (rhs) of the given rule. In our example the rule has two rewrites: 
\begin{figure}[h]
\centering
\begin{tabular}{ l c  r }
\begin{minipage}{.2\textwidth}
\footnotesize
\begin{verbatim}  spawn => .\end{verbatim} 
\end{minipage}&
and 
& \begin{minipage}{.62\textwidth}
\footnotesize
\begin{alltt}
        (. => <thread_> 
                 \textcolor{red}{<k> S </k> <env> Env </env>}                                                                               
            <_/thread>)
\end{alltt}
\end{minipage}\\
\end{tabular}
\end{figure}
If the first one is a simple rewrite of a statement the second one is a cell creation. The dot "." in the lhs is the neutral element of the sort of the cell; rewriting "." in something is the equivalent of creation/construction of a new K term. The main difficulty in general is to determine the context of "." because of the lack of information. In our case we can disambiguate using the rhs of the rule where we find the {\it thread} cell and we can infer that "." is at the same level with {\it thread} (in the sense that they could have the same parent cell). Also, in disambiguation process, context transformers should care about the other components of the rule. For example, if we look again at thread creation rule we can observe that the other {\it thread} cell (corresponding to the first rewrite) could be relevant when finding the full context. 
\begin{figure}[h]
\centering
\begin{tabular}{| l | r |}
\hline
\begin{minipage}{.45\textwidth}
\footnotesize
\begin{verbatim}
configuration 
       <T>
          <a> 
             <b> 
                <c>
                   <d*> .Bag </d>
                </c>
             </b>
             <y>
                <z>
                   <d> .Bag </d>
                </z>
             </y>
          </a>
      </T>
\end{verbatim}
\end{minipage}
\begin{tabular}{l}
\begin{minipage}{.45\textwidth}
\footnotesize
\begin{verbatim}
rule <b> 
        . => <d> .Bag </d> 
     </b>
\end{verbatim}
\end{minipage}\\\\
\hline\\
\begin{minipage}{.45\textwidth}
\footnotesize
\begin{verbatim}
rule <T>
        <a>
           <b>
              <c>  
               . => <d> .Bag </d> 
              </c>
           </b>
        </a>
     </T>
\end{verbatim}
\end{minipage}
\end{tabular}\\
\hline
\end{tabular}
\caption{Configuration, K rule and rewrite rule}
\label{example:one}
\end{figure}
Figure \ref{example:one} contains an example of a K rule (top right) and its context (bottom right) according to a configuration (left). This is the most general behavior which context transformers should have: detect in the configuration all the cells that appear in the rule and append missing cells. In the previous example (thread creation rule in SIMPLE) context transformers added only cells above cell {\it thread} which was the top of the rule. Here we have to add cells inside the rule not only on the top of it. Cells {\it b} and {\it c} were added on the top of {\it d} and {\it T} was added above {\it a}. Also, note that this configuration contains two cells with the same name or label: {\it d}. In this case its very easy to determine that cell {\it d} is that cell {\it d} under {\it b} and not that cell {\it d} under {\it y}. 
\begin{figure}[h]
\centering
\begin{tabular}{| l | r |}
\hline
\begin{minipage}{.45\textwidth}
\footnotesize
\begin{alltt}
configuration 
       <T>
          <a> 
             <b> 
                <c>
                   <d*> .Bag </d>
                </c>
             </b>
             <y>
                <z>
                   \textcolor{red}{<d> .Map </d>}
                </z>
             </y>
          </a>
      </T>
\end{alltt}
\end{minipage}
\begin{tabular}{l}
\begin{minipage}{.45\textwidth}
\footnotesize
\begin{alltt}
rule <\textcolor{red}{a}> 
        . => <d> .Bag </d> 
     </\textcolor{red}{a}>
\end{alltt}
\end{minipage}\\\\
\hline\\
\begin{minipage}{.45\textwidth}
\footnotesize
\begin{verbatim}
rule <T>
        <a>
           <b>
              <c>  
               . => <d> .Bag </d> 
              </c>
           </b>
        </a>
     </T>
\end{verbatim}
\end{minipage}
\end{tabular}\\
\hline
\end{tabular}
\caption{Configuration, K rule and rewrite rule}
\label{example:two}
\end{figure}
The content of  Figure \ref{example:two} is almost similar with content shown in Figure \ref{example:one}; the only differences are that cell {\it d} under {\it z} in the configuration changed its type into {\it Map} and in the rule cell {\it b} was replaced with cell {\it a}. Note that the rule is now ambiguous from the point of view of cell nesting because cell {\it a} contains cell {\it d} twice. Context transformers should report such ambiguities and this implies that is should look for all the ambiguous constructs. This fact could add more complexity to the transformation algorithm. More than that, our example is not ambiguous at all: we can observe that inside cell {\it a} is created cell {\it d} which has the type \verb=.Bag=. The other cell {\it d} inside {\it a} has the type \verb=.Map= in the configuration which is not the type of cell {\it d} in the rule. Again, this kind on disambiguation could add a higher degree of complexity for transformation algorithm.
\begin{figure}[h]
\centering
\begin{tabular}{| l | r |}
\hline
\begin{minipage}{.45\textwidth}
\footnotesize
\begin{alltt}
configuration 
       <T>
          <a> 
             <b*> .Map </b>
             <o> .Map </o>
          </a>
          <y>
             <z> .Set </z>
             <o> .Map </o>
          </y>
      </T>
\end{alltt}
\end{minipage}
\begin{tabular}{l}
\begin{minipage}{.45\textwidth}
\footnotesize
\begin{alltt}
 rule <o> M:Map </o> 
     (. => <b> M </b>) 
\end{alltt}
\end{minipage}\\\\
\hline\\
\begin{minipage}{.45\textwidth}
\footnotesize
\begin{verbatim}
rule <T>
        <a>
        	<o> M:Map </o>
	        (. => <b> M </b> )
        </a>
     </T>
\end{verbatim}
\end{minipage}
\end{tabular}\\
\hline
\end{tabular}
\caption{Configuration, K rule and rewrite rule}
\label{example:three}
\end{figure}
There are also other levels of disambiguation. Solving the context for a rule can be done in two ways:
\begin{enumerate}
\item split the rule into lhs and rhs, apply contextual transformations on each of them and then combine the solutions
\item do not split the rule and try to solve contexts on pieces determined by rewrites
\end{enumerate}
The second variant is used in the current algorithm but it seems that it determined a very complicated and hard to maintain algorithm. Also, it was designed using the bottom-up algorithm and it could be difficult to redesign it using the top-down approach. In first variant, the separation of a rule into lhs and rhs to apply contextual transformations on them implies also their combination in the end. The advantage of this approach is that the algorithm which appends cells on a given rule according to a configuration is very clear. The disadvantage is that we have to combine the context for both sides and this implies disambiguation also at this level. This combination can be reduced to finding the rewrite "points": those cells inside a rule which contain rewrites. 
Finding those rewrites is not necessarily an easy task but it can be done by storing as much information as possible from the parsing tree of the rule. The rule given in Figure \ref{example:three} is split into: rhs (which contains the cell {\it b}) and lhs (which doesn't contain {\it b}). Consider that both sides are filled with context. First, for lhs we can obtain two available trees:
\begin{figure}[h]
\centering
\begin{tabular}{ l c  r }
$a_1)$    \begin{minipage}{.3\textwidth}
\footnotesize
\begin{verbatim}
   <a>
      <o> M:Map </o>
   </a>
</T>
\end{verbatim} 
\end{minipage}&
and 
& $b_1)$
\begin{minipage}{.3\textwidth}
\footnotesize
\begin{verbatim}
   <y>
      <o> M:Map </o>
   </y>
</T>
\end{verbatim} 
\end{minipage}\\
\end{tabular}
\end{figure}
For the rhs there are also two possible trees:
\begin{figure}[h]
\centering
\begin{tabular}{ l c  r }
$a_2)$ 
\begin{minipage}{.3\textwidth}
\footnotesize
\begin{verbatim}
   <a>
      <o> M:Map </o>
      <b*> M </b>
   </a>
</T>
\end{verbatim} 
\end{minipage}&
and 
& $b_2)$
\begin{minipage}{.3\textwidth}
\footnotesize
\begin{verbatim}
   <a>
      <b> M </b>
   </a>
   <y>
      <o> M:Map </o>
   </y>
</T>
\end{verbatim} 
\end{minipage}\\
\end{tabular}
\end{figure}
Obviously, $a_2)$ is the right context for the given rule. The difficulty is to find the inferences which should be done in order to determine it in the most general case. Here we can deduce that cells {\it o} and {\it b} are at the same level and this is why we choose $a_2)$ instead of $b_2)$. Of course, we have to determine the compatible pair from lhs; here the pairs are ($a_1$, $a_2$) and ($b_1$, $b_2$) with the motivation that the corresponding trees could be merged without losing rule consistency. 
Another reason to choose $a_2)$ is given by the {\it locality principle}. This principle says that the context of a rule should be {\it as local as possible} and this implies somehow the idea that the context should be defined by {\it the most grouped} tree. Intuitively, we can also say that the context of a rule should contain a minimal number of nodes but this may lead to another problems and could not be used as being the locality principle criteria for disambiguation.












\section{Analyzing and formalizing contextual transformations}
In this section we will discuss a top down approach for finding an algorithm for contextual transformations and we also give some formal definitions to define the concepts.
\subsection{Matchings}
\label{matching}
In a K {\it configuration}, cells can be nested or not. A nested structure can be seen as a tree structure where each $cell$ is represented by a $node$ in the tree. In most cases the {\it configuration} contains only a nesting but K allows $configurations$ which contain multiple nestings or simple cells which are not nested. Of course, $rules$ are strongly linked to {\it configuration} structure. In order to find a common data structure for both $configurations$ and $rules$ we associate for each nesting or single cell a tree and we obtain a \textit{forest of trees}. Each $node$ in this forest contains informations about its corresponding cell. A \textit{configuration forest} $F_C$ corresponds to a K configuration and a node $n_{F_C} \in F_C$ contains the cell name, the assigned multiplicity and the nested cells if any. A \textit{rule forest} $F_R$ corresponds to a K rule and a node $n_{F_R} \in F_R$ contains the cell name, informations about open cells and nestings if any.
\begin{figure}[h]
\centering
\begin{tabular}{| c |}
\hline
\begin{minipage}{.8\textwidth}
\footnotesize
\begin{alltt}
 configuration
    <T>
      <agent multiplicity="*"> 
          <control>
              <thread multiplicity="*">
                  <k>.K</k>
                  <nextId>0</nextId>
                  <holds>.Map</holds>
              </thread>
          </control>
          <busy>.Set</busy> 
          <mem> .Map </mem> <nextLoc> 0 </nextLoc>
          <me>0</me>
          <parent>-1</parent>
      </agent>
      <nextAgent>1</nextAgent>
      <world>SetItem(0)</world>
      <barrier>true</barrier> <waiting>.Set</waiting>
      <messages> <message multiplicity="*">
          <from>.K</from> <to>.Set</to> <body>.K</body>
      </message> </messages>
      <I-O> <in>.List</in> <out>.List</out> </I-O>
    </T>
\end{alltt}
\end{minipage}\\
\hline
\end{tabular}
\caption{AGENT (modified) configuration}
\label{agent:config}
\end{figure}
% configuration tree for agent
\begin{figure}
\centering
\begin{tikzpicture}
% edges from T to subtrees
\draw (0,5) node[anchor=south,circle,draw]{T} -- (-5,3) node[anchor=north,circle,draw]{agent};
\draw (0,5) node[anchor=south,circle,draw]{T} -- (-3,3) node[anchor=north,circle,draw]{nextAgent};
\draw (0,5) node[anchor=south,circle,draw]{T} -- (-1,3) node[anchor=north,circle,draw]{world};
\draw (0,5) node[anchor=south,circle,draw]{T} -- (1,3) node[anchor=north,circle,draw]{barrier};
\draw (0,5) node[anchor=south,circle,draw]{T} -- (3,3) node[anchor=north,circle,draw]{waiting};
\draw (0,5) node[anchor=south,circle,draw]{T} -- (5,3) node[anchor=north,circle,draw]{messages};
\draw (0,5) node[anchor=south,circle,draw]{T} -- (7,3) node[anchor=north,circle,draw]{I-O};
% subtree for agent
\draw (-5, 1.65) -- (-5, 0);
\draw (-5,0) -- (-5.5, -1) -- (-4.5, -1) -- (-5,0);
% subtree for messages
\draw (5, 1.05) -- (5, 0);
\draw (5, 0) -- (4.5,-1) -- (5.5, -1) -- (5, 0);
% subtree for I-O
\draw (7, 1.96) -- (7, 0);
\draw (7, 0) -- (6.5, -1) -- (7.5, -1) -- (7, 0);
\end{tikzpicture}
\caption{Configuration tree corresponding to AGENT configuration}
\label{agent:configtree}
\end{figure}
At this point we can talk about \textit{configuration trees} and \textit{rule trees}, which are trees derived from \textit{configuration forest}, respectively \textit{rule forest}, by adding a node $T$ and edges between this node and roots of each tree from corresponding forest. For example, the corresponding tree for AGENTS's modified configuration (Figure \ref{agent:config}) is shown in Figure \ref{agent:configtree}. The configuration tree is obtained by adding node $T$ and edges from $T$ to each tree in the forest: $(T, agent)$, $(T, nextAgent)$, $(T, world)$, $(T, barrier)$, $(T, waiting)$, $(T, messages)$, $(T, I-O)$. A clone of node ($T$) is then combined in the same way with each \textit{rule forest} to get the corresponding \textit{rule tree}. We will see in the next sections that adding the same node $T$ as root for both configuration and rule trees makes the algorithm easier to describe.
Also, the {\it configuration} can be seen as a \textit{pattern} for a rule and in order to get its context, we have to find if this pattern \textit{matches} the rule and to determine what cells from the pattern(configuration) are missing in the rule. Therefore, if $C$ is a \textit{configuration tree} and $R$ is a \textit{rule tree} we can say that $C$ (the pattern) $matches$ $R$ if each node (cell) in $R$ is $similar$ to a node (cell) in $C$ and nestings in $R$ can be found as paths in $C$. Definition \ref{matching} specifies a recursive definition for a \textit{matching} which says that a \textit{matching} between a \textit{configuration tree} and a \textit{rule tree} reduces to \textit{similarity} of their roots and the $matching$ of their subtrees, while matching subtrees means finding matchings for each subtree. \\
\begin{defn}
Let C be a \textit{configuration tree} and R a \textit{rule tree}. We say that \textit{C matches R} and we denote it $C \prec R$ if: 
$$C \prec R \Leftrightarrow root(C) \sim root(R) \wedge subtrees(C) \llcurly subtrees(R), $$
where $root(T)$ is the root of tree $T$ and $subtrees(T)$ is the set of all subtrees of $T$. \\
Let $subtrees(C)  = \{C_1, C_2, ..., C_p\}$ and $subtrees(R)  = \{R_1, R_2, ..., R_q\}$ then:
$$C_1, C_2, ..., C_p \llcurly R_1, R_2, ..., R_q \Leftrightarrow (\bigvee_{i=\overline{1,p}}{ \dots, subtrees(C_i), \dots \llcurly R_1, \dots, R_q}) $$ 
$$\vee (\bigvee_{C_i \prec R_j}{\dots, C_{i-1},C_{i+1}, \dots \llcurly \dots, R_{j-1}, R_{j+1}, \dots ) .} $$
\label{matching}
\end{defn}
In order to define $similarity$ of two nodes we have to specify exactly what is a $node$. There are two different types of nodes: \textit{configuration nodes} and \textit{rule nodes}; in other words, there is a different type of node for each type of tree. A \textit{configuration tree} (\textit{rule tree}) is made up by \textit{configuration nodes} (\textit{rule nodes}) and links between them which correspond to nestings in {\it configuration} ({\it rule}). Actually, these nodes have some common attributes like: unique identifier, cell label, additional data and links to parent node and children nodes. The definition of a node is given in  Definition \ref{node}.\\
% node
\begin{defn}
Let $c$ be a K $cell$ and $T=(N_T,E_T)$ a tree, where $N_T$ is the set of nodes and $E_T$ is the set of edges. 
Node $n \in V_T$  corresponds to cell $c$ if $n=(id, label, data, parent, children)$, where: 
\begin{array}{l}
\qquad \text{ - } id\in \mathbb{N}^*\text{ is the unique identifier for the current node,}\\ 
\qquad \text{ - } label \text{ is the label of $c$,}\\ 
\qquad \text{ - } data \text{ is content of $c$,}\\ 
\qquad \text{ - } parent \in \mathbb{N}^* \cup \{null\}\text{ is the id of its parent node,} \\
\qquad \text{ - } children \subseteq (\mathbb{N}^*)^n \cup \{null\}\text{ is a list of ids which correspond to all}\\
\qquad \qquad \text{ children of the current node.} \\
\qquad \text{ - }  type\in KTypes \text{ is the type of the cell.}
\end{array}
We say that {\it id}, {\it label}, {\it data}, {\it parent}, {\it children}  and {\it type} are fields of node {\it n} and we will denote a field by qualifying the node name with ".". For example {\it n.id} refers to field {\it id} of node {\it n}.
Also, {\it KTypes} is given by:
$$KTypes=\{Bag, Set, List, Map, K\}.$$
\label{node}
\end{defn}
The difference between \textit{configuration node} and \textit{rule node} is given by the fact that a {\it configuration} is a pattern and it contains some specific data, like multiplicity or cell type. A {\it rule} specifies only the rewriting rules inside a {\it configuration} but not the multiplicity of a cell or its data type. In Propositions \ref{node:config} and \ref{node:rule} we construct the specific structure of \textit{configuration node} and \textit{rule node} considering $node$ defined as in Definition \ref{node}.\\
\begin{proposition}
Be $n$ a node as defined in Definition \ref{node}. We construct a \textit{configuration node} from $n$ by adding fields \textit{multiplicity}, \textit{inherited} multiplicity and \textit{type}.
\label{node:config}
\end{proposition}
Let $c$ be a \textit{configuration node}. The meaning of its specific fields is the following:
\begin{itemize}
\item {\it n.multiplicity $\in$ \{ANY, SOME, MAYBE, NONE\}} - is the multiplicity for its corresponding cell given by the user in the configuration.
\item {\it n.inherited $\in$ \{ANY, SOME, MAYBE, NONE\}} - represents the inherited multiplicity for the current node. This kind of multiplicity is deduced by considering all the multiplicities of its ancestors and its proper multiplicity, and it is very useful to determine which is the context of current cell. If cell has an ancestor which has multiplicity {\it ANY} then that cell can appear into a rule multiple times even if its proper multiplicity is {\it NONE} or {\it MAYBE}. But, in this case, for each occurrence of current node we have to get the separate contexts until we reach that ancestor.
\end{itemize}
\begin{proposition}
Be $n$ a node as defined in Definition \ref{node}. We construct a \textit{rule node} from $n$ by adding fields \textit{occurrences} and \textit{open}.
\label{node:rule}
\end{proposition}
Let $r$ be a \textit{rule node}. The meaning of its specific fields is the following:
\begin{itemize}
\item $n.occurrences \in \mathbb{N^*}$ - represents the number of occurrences for $n.label$ under $n.parent$.  For example in rule shown in Figure \ref{rule:sample} both cells $<$a$>$ under cell $<$k$>$ correspond to the same cell given in the configuration with multiplicity \textit{ANY}. Cell $<$a$>$ which is not under $<$k$>$ can correspond to any other cell in the configuration which is labelled with $a$ but not to a cell under $<$k$>$. This means that $a.occurrences = 2$ for cell $<$a$>$ contained by $<$k$>$ and $a.occurrences = 1$ for the single cell $<$a$>$. 
\item $n.open \in \{left, right, both, none\}$ - specifies if the corresponding cell in the configuration is open at left, right, both sides or it is not open.
\end{itemize}
% sample rule
\begin{figure}
\centering
\fbox{
\begin{minipage}{\textwidth}
\begin{tabbing}
rule \=$<$k$>$\=\\
\>\>$<$a$>$ sample1 =$>$ sample11 $<$/a$>$\\
\>\>$<$a$>$ sample2 =$>$ sample22 $<$/a$>$\\
\>$<$/k$>$\\
\>$<$a$>$ sample3 =$>$ sample33 $<$/a$>$\\
\end{tabbing}
\end{minipage}
\caption{Sample rule}
\label{rule:sample}
\end{figure}
% similar
Now we can define the $similarity$ relation between a \textit{configuration node} $c$ and a \textit{rule node} $r$. Definition \ref{similarity} says that \textit{c is similar with r} if they have the same label and the number of occurrences for $b$ is smaller than inherited multiplicity of $a$.\\
% similarity
\begin{defn}
Let $c$ be a \textit{configuration node} and $r$ a \textit{rule node}. We say that \textit{c is similar with r} and we denote it $c \sim r$ if:
%$$c \sim r \Leftrightarrow c.label = r.label \wedge c.inherited \geq r.occurrences \wedge c.type = r.type$$
$$c \sim r \Leftrightarrow c.label = r.label \wedge c.type = r.type$$
\label{similarity}
\end{defn}
When a user gives a rule in a K definition it is very likely that the rule is matched more than once by the configuration. Therefore, we have to collect all matchings in order to decide which of them should be chosen to represent the final context for the given rule. In Definition \ref{witness} the set {\it M} is called {\it witness} of a matching if it contains a valid matching: for each node {\it r} in rule tree we have a pair $c \mapsto r$ where {\it c} is a configuration node and $c \sim r$. In other words, a {\it witness} contains pairs {\it (c, r)} for each node {\it r} and these pairs can be used to determine the context of a rule by using the {\it parent} field. If a rule has more than one matching then it will have more {\it witnesses}. A set of {\it witnesses} is defined in Definition \ref{witnessset}.\\
% witness
\begin{defn}
Let {\it C} be a {\it configuration tree} and {\it R} a {\it rule tree}. We say that set {\it M is witness of C $\prec$ R} if:
$$\text{\it M witness of } C \prec R \Leftrightarrow $$
$$M = \{(\textit{root}(C) \mapsto \textit{root}(R)) \cup M' \mid M' \textit{witness of subtrees(C)} \llcurly \textit{subtrees(R)}\}$$
Let $subtrees(C)  = \{C_1, C_2, \dots, C_p\}$ and $subtrees(R)  = \{R_1, R_2, \dots , R_q\}$ then:
$$\textit{M witness of } C_1, \ldots , C_p \llcurly R_1, \dots, R_q \Leftrightarrow$$
$$(\exists i) (\textit{M witness of } \ldots, subtrees(C_i), \ldots \llcurly R_1, \dots, R_q)  \vee$$
$$(M = M' \cup M'' \wedge (\exists i, j) (M' \textit{ witness of } C_i \prec R_j \wedge$$
$$M''\textit{ witness of } \ldots, C_{i-1}, C_{i+1}, \ldots \llcurly \ldots R_{j-1}, R_{j+1} \ldots ))$$
\label{witness}
\end{defn}
% witness set
\begin{defn}
Let {\it C} be a {\it configuration tree} and {\it R} a {\it rule tree}. A witness set is defined as follows:
$$\textit{WitnessSet}(C \prec R)=\{M \mid M \in WitnessSet(subtrees(C) \llcurly subtrees(R))\}$$
$$\textit{WitnessSet}(C_1, \ldots , C_p \llcurly R_1, \dots, R_q) = (\bigcup_{i=\overline{1,p}} WitnessSet( \ldots subtrees(C_i) \ldots $$
$$\llcurly R_1, \ldots, R_q )) \cup (\bigcup_{C_i \prec C_j} WitnessSet(\ldots, C_{i-1}, C_{i+1}, \ldots \llcurly \ldots R_{j-1}, R_{j+1} \ldots ))$$ 
where $subtrees(C)  = \{C_1, C_2, \dots, C_p\}$ and $subtrees(R)  = \{R_1, R_2, \dots , R_q\}$.
\label{witnessset}
\end{defn}
The Function \ref{a1} computes the set of witnesses for a given rule and its corresponding configuration. Arguments {\it configuration} and {\it rule} are the root nodes of configuration and rule trees. First, the function search the label of rule root in the configuration and puts all the nodes found in the set {\it N}. Each node in this set should be valid in the sense that a node $n \in N$ corresponds exactly to root node of the rule; for example, valid nodes should have the same type. This validation is done by function {\it validate(N)} which checks foreach $n\in N$ if $n \sim rule$. If there are no valid nodes, then the function will return the empty set. If the set {\it N} is not empty after validation then we have to add pairs {\it (n, rule)} where $n\in N$ in each witness found so far. In case rule has children then we have to solve the children recursively first: function {\it append()} returns all the combinations of witnesses for children and then we can append each pair to each witness found.
Function \ref{a1} needs some preconditions in order to return the expected results: the set of labels from rule tree should be included in the set of labels from configuration tree. This inclusion could be checked before function \ref{a1} is called; it was not included in the function because we want to keep its semantics as simple as possible. Another precondition is related to existence of valid nodes in the configuration for each node in the rule. This precondition is strongest than the first one and ensures that the set of witnesses doesn't contain any incomplete witness: nodes from rule tree which have no corresponding node in configuration. Actually, in K, a rule makes sense when such a precondition is satisfied. Otherwise, one can postprocess the obtained witnesses to return a nice error message.
\begin{function}
\SetKwInOut{Input}{Input}\SetKwInOut{Output}{Output}
\Input{configuration, rule - trees}
\Output{M - set of witnesses}
\Begin{
	N = configuration.searchNodesByLabel(rule.label)\;
	N = validate(N)\;
	M = $\emptyset$\;
	\uIf{N = $\emptyset$}
	{\Return $\emptyset$\;}
	\eIf{rule.children $\neq$ $\emptyset$}
	{%then
		\For{n $\in$ N}
			M$_i$ = \{n\}\;
			M = M $\cup$ \{ M$_i$ \}\;
	{%else
		\For{n $\in$ N}
			wSet = $\emptyset$\;
			\For {r $\in$ rule.children}
			{
				sons = \ref{a1}(n, r)\;
				\uIf{sons $\neq$ $\emptyset$}
				{
					wSet = append(wSet, sons)\;
				}
			}
			\uIf{wSet $\neq$ $\emptyset$}
			{
				\For {m $\in$ wSet}
				{
					M = M $\cup$ \{\{(c,rule)\} $\cup$ m\}\;
				}
			}
	\Return{M}\;
\caption{findAllWitnesses(configuration, rule)}
\label{a1}
\end{function}
The function traverses only once the rule tree but for each node in the rule tree we have to traverse the configuration tree which implies \ref{a1} $\in O(m \times n)$, where {\it m} is the number of nodes from rule tree and {\it n} the number of nodes from configuration tree. 
\subsection{Cell completion}
Contextual transformation is about adding the missing cells to a rule according to a given configuration. In our formalism a rule or a configuration is transformed into a tree. We already have a method (witness) to find which nodes from configuration tree correspond to nodes from rule tree and we can use this to fill the rule tree with missing nodes from configuration.
\begin{function}
\SetKwInOut{Input}{Input}\SetKwInOut{Output}{Output}
\Input{P - path, T - tree}
\Output{result - set of trees}
\Begin{
	Be n the bottom most common node of P and T\;
	result = $\emptyset$\;
	\uIf{T = null}
	{\Return \{P\}\;}
	\While{n $\neq$ root(tree)}
		\eIf{n.multiplicity $\in$ \{NONE, MAYBE\}}
		{ %then
			merge P in n to T\;
			result = result $\cup$ T\;
			break\;
		{ %else
			\tcp{n.multiplicity $\in$ \{NONE, MAYBE\}}
			T' = T\;
			merge P in n to T'\;
			result = result $\cup$ T'\;
			n = n.parent\;
	\Return{result}\;
\caption{mergePathToTree(path, tree)}
\label{a3}
\end{function}
Consider we have a rule R, a configuration C and a witness W. Now, for each edge from R we can find a path in C using W easily: if {\it (a,b)} is an edge we can get from W a pair of nodes {\it (a$_c$, b$_c$)} which describe a path in the configuration. If we do that for each edge then we can get the corresponding tree for R. 
In Figures \ref{config:tree} and \ref{rule:tree} we have an example of a configuration tree and a rule tree with its corresponding context. The main difficulty in getting the context is to combine the paths corresponding to each edge of the rule tree. In our case we have the following paths:
\begin{itemize}
\item $(a,c)$ corresponds to $Path_1=(\{a,d,c\}, \{(a,d);(d,c)\})$.
\item $(a,f)$ corresponds to $Path_2=(\{a,b,z,f\},\{(a,b);(b,z);(z,f)\})$.
\item $(a,f)$ corresponds to $Path_3=(\{a,b,z,f\},\{(a,b);(b,z);(z,f)\})$.
\end{itemize}
Edge $(a,f)$ appears twice and this is possible because $f$ has inherited multiplicity $ANY$. We can see in the resulting tree (which is shown on the right hand side of Figure \ref{rule:tree}) that cell $f$ appears twice by duplicating cell $z$.
% configuration tree for agent
\begin{figure}
\centering
\begin{tikzpicture}
% edges from a to subtrees
\draw (-3,5) node[anchor=south,circle,draw]{a} -- (-5,4) node[anchor=north,circle,draw]{d};
\draw (-3,5)  -- (-1,4) node[anchor=north,circle,draw]{b*};
% edges from c
\draw (-5,3.22) -- (-6,2.5) node[anchor=north,circle,draw]{c};
\draw (-5,3.22) -- (-4,2.5) node[anchor=north,circle,draw]{t};
% edges from b*
\draw (-1,3.08) -- (-2,2.5) node[anchor=north,circle,draw]{z*};
\draw (-1,3.08) -- (-1,2.5) node[anchor=north,circle,draw]{c};
\draw (-1,3.08) -- ( 0,2.5) node[anchor=north,circle,draw]{u};
% edges from z
\draw (-2,1.61) -- (-2,1) node[anchor=north,circle,draw]{f};
% edges from u
\draw (0,1.79) -- (0,1) node[anchor=north,circle,draw]{t};
\end{tikzpicture}
\caption{Configuration tree sample}
\label{config:tree}
\end{figure}
% configuration tree for agent
\begin{figure}
\centering
\begin{tikzpicture}
% left hand side: only the rule
% edges from a to subtrees
\draw (-3,5) node[anchor=south,circle,draw]{a} -- (-5,4) node[anchor=north,circle,draw]{c};
\draw (-3,5)  -- (-2,4) node[anchor=north,circle,draw]{f};
\draw (-3,5)  -- (0,4) node[anchor=north,circle,draw]{f};
% right hand side: the context for the given rule
% edges from a to subtrees
\draw (4,5) node[anchor=south,circle,draw]{a} -- (2,4) node[anchor=north,circle,draw]{d};
\draw (4,5) -- (6,4) node[anchor=north,circle,draw]{b};
% edges from d
\draw (2,3.25) -- (2,3) node[anchor=north,circle,draw]{c};
% edges from b
\draw (6,3.24) -- (5,3) node[anchor=north,circle,draw]{z};
\draw (6,3.24) -- (7,3) node[anchor=north,circle,draw]{z};
% edges from z
\draw (5,2.31) -- (5,2) node[anchor=north,circle,draw]{f};
\draw (7,2.31) -- (7,2) node[anchor=north,circle,draw]{f};
\end{tikzpicture}
\caption{Rule sample and its corresponding context}
\label{rule:tree}
\end{figure}
There are more than one possible trees which can be obtained in this manner because of multiplicity associated to each node. When building the corresponding tree T paths need to be merged one by one; consider a path P which has five nodes and they have multiplicities (in this order): {\it a$_1$ - NONE}, {\it a$_2$ - ANY}, {\it a$_3$ - NONE}, {\it a$_4$ - ANY}, {\it a$_5$ - NONE}; also consider that path from {\it a$_1$} to {\it a$_4$} is common for P and T and only {\it a$_5$} has to be added in T. There are a few possible solutions:
\begin{itemize}
\item append {\it a$_5$} as a child of {\it a$_4$} ($\in$ T) if {\it a$_5$} is not already a child of {\it a$_4$}.
\item append {\it a$_4$} and the rest of P as a child of {\it a$_3$} ($\in$ T) because {\it a$_4$} has multiplicity {\it ANY} or {\it SOME}.
\item append {\it a$_2$} and the rest of P as a child of {\it a$_1$} ($\in$ T) because {\it a$_2$} has multiplicity {\it ANY} or {\it SOME}.
\end{itemize}
This algorithm is implemented by Function \ref{a3} which receives as input a path {\it P} and returns the set of all possible trees obtained by merging {\it P} to {\it T}. 
\begin{function}
\SetKwInOut{Input}{Input}\SetKwInOut{Output}{Output}
\Input{C, R - configuration and rule trees}
\Output{allTrees - set of trees}
\Begin{
	allTrees = $\emptyset$\;
	wSet = \ref{a1}(C, R)\;
	\For{w $\in$ wSet}
		wTemp = $\emptyset$\;
		\tcp{for each edge in R tree get the corresponding}
		\tcp{path from configuration (C) and return}
		\tcp{all possible trees}
		\For{edge $\in$ R}
		{ 
			path = getPath(edge, C, w)\;
			\eIf{wTemp = $\emptyset$}
			{
				wTemp = \{ path \}\;
			}
			{
				\For{tree $\in$ wTemp}
				{
					wTemp = wTemp - \{tree\}\;
					wTemp = wTemp $\cup$ \ref{a3}(path, tree)\;
				}
			}	
		allTrees = allTrees $\cup$ wTemp\;
	\Return{allTrees}\;
\caption{getAllTrees(C, R)}
\label{a2}
\end{function}
Now, we have everything we need to get all trees which correspond to a rule. Function \ref{a2}
computes the set of all trees for the whole set of witnesses. For each witness, the function computes all possible trees by calling the merging function \ref{a3} and all the results are stored in a set which will be returned in the end. 
Regarding execution time estimation, Function \ref{a3} traverses in a bottom-up manner a path
and copies a tree into another tree in a linear time when a node with multiplicity {\it ANY} or {\it SOME} is found. This implies \ref{a3} $\in$ {\it O(n$^2$)}, where {\it n} is the number of nodes in the rule. Because Function \ref{a2} calls \ref{a1} and \ref{a2} and it doesn't contain any recursion its execution time is polynomial.\\
\subsection{Minimal context}
The contexts we find using \ref{a2} are complete, in the sense that all of them contain the top cell as it is in configuration. Some execution backends like OCaml need the whole context of a rule to execute it. Others, like Maude, works much better if only the minimal context is provided. The minimal context is defined in Definition \ref{minimal}.
\begin{defn}
Be C a configuration, R a node, R' the context for R and r $\in$ R'. We say r is the minimal context for R if:
\begin{itemize}
\item $(\forall n \in$ R) ($n \in$ r)
\item r $\in$ R $\vee$ $(!\exists r'\in Ancestors(r))(|r'.children| > 1)$
\end{itemize}
\label{minimal}
\end{defn}
This definition says that r is represents the minimal context if it is the first common ancestor for all the nodes from rule or if it is already in the rule but still contains all the other nodes too. An algorithm which computes the minimal context should start iterating from the root of the configuration down through the nodes until it finds a node which has more than one child or a node from rule tree. This is very easy and can be done in linear time.
\section{Filters}
For each rule we can determine all possible (minimal) contexts using function \ref{a2}. The target now is to get the most relevant from all these because the compiler needs only one context for each rule. To do so, we apply some filters over the set of contexts until we reach only one context. After filtering, if the set of contexts contains more than one context then an ambiguity should be reported and the compilation stops. In this section we discuss the locality principle and we propose some filters in order to choose the right context.
\subsection{Locality Principle}
The locality principle represents the main criterium to choose between contexts. It makes more sense when minimal contexts are used and it is described in \cite{jlap2010} as follows:\\
{\it" ... locality principle: rules are transformed in a way that makes them as local as possible, or, in other words, in a way that the resulting rule matches as deeply as possible in the concrete configuration."}\\
As we can observe this intuitive definition is not formal at all. Here, we will try to define some criteria which could help us in finding a complete definition for locality principle.
\begin{enumerate}
\item Smallest number of nodes. We can compute the number of nodes of each tree and choose the ones which have the smallest number. The motivation of using such a filter is given by the fact that smaller trees are more compact than the other: a smaller number of nodes in a tree implies a smaller number of edges. But, this method does not offer any guarantee regarding the sentence "{\it as deep as possible}".
\item Compute the "deepness" of the minimal context. When the minimal context r is determined, one can compute the distance h from the root of the configuration to r. Once this distance is computed we can do a descending sort by h on the list of contexts and get the first context. This is the equivalent of choosing the "deepest" minimal context. Again, this method doesn't verify how compact the contexts are.
\end{enumerate}
Event if it seems that each of these variants doesn't satisfy the definition given in \cite{jlap2010} for locality principle, we can obtain a definition for locality principle by combining them. 
\begin{defn}
Be T the set of all minimal contexts (trees) for a rule and t $\in$ T. We also consider functions {\it size()} and {\it height()} which compute the number of nodes for a tree and respectively the {\it deepness} of the minimal context in configuration. We say that t respects the locality principle if:
$$size(t)=min({size(t')|t'\in T}) \wedge height(t)=max({height(t')|t'\in T}).$$
\end{defn}
The locality principle can act right now as a filter which could be applied on the set of all minimal contexts.
\subsection{Consistency filters}
Consistency filters are a special category of filters which should be applied right after minimal contexts are computed. Consistency checks are taking care that all results given by function \ref{a2} are not wrong. There are two types of checks:
\begin{enumerate}
\item Multiplicity consistency. This check detects those cases when one uses two cells with the same label at the same level in rule and these two cells are not marked with multiplicity {\it ANY} or {\it SOME} in configuration. If that cell label doesn't appear twice on different paths in the context then it is not consistent and has to be removed.
\item Cell contents consistency. This is more like a disambiguation step. Consider a configuration which contains cell {\it c} in two different places: under cell {\it a} which also contains other cells and under cell {\it b} which contains only cell {\it c}. Also, cells {\it a} and {\it b} are under cell {\it T}. When a user specifies in a rule cell {\it c} under {\it T} then we can say that cell {\it c} which is the only one specified inside {\it T} is that cell from {\it b} and not the one from {\it a} because {\it a} also contains other cells. So, this step chooses in some sense {\it the most local} variant avoiding the open cells if possible.
\end{enumerate}
\subsection{Applying filters}
In order to get the unambiguous context for a rule we have to apply all the filters we discussed in the previous subsections.
\begin{function}
\SetKwInOut{Input}{Input}\SetKwInOut{Output}{Output}
\Input{C, R - configuration and rule trees}
\Output{context - minimal context for R}
\Begin{
	contexts = \ref{a2}(C,R)\;
	contexts = getMinimalContexts(contexts)\;
	contexts = applyConsistencyFilters(contexts)\;
	contexts = applyLocalityPrinciple(contexts)\;
	\tcp{return the final context}
	\uIf{|contexts| = 1}
		Be context $\in$ contexts\; 
		\Return{context\;}
	\tcp{ambiguous context}
	\Return null;
\caption{getContext(C, R)}
\label{a4}
\end{function}
Function \ref{a4} returns the final context of a rule R according to configuration C. It gets all possible minimal contexts, applies filters on them and returns the context if the rule is not ambiguous.